0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 24 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 50 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 MRRProof (⇔, 41 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U4_GA(T27, T28, T29, append1C_in_ga(T28, X27))
PERME_IN_GA(.(T27, T28), .(T27, T29)) → APPEND1C_IN_GA(T28, X27)
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U5_GA(T27, T28, T29, append1C_in_ga(T28, T31))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_GA(T27, T28, T29, permE_in_ga(T31, T29))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(.(T45, T46), .(T47, T48)) → U7_GA(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
PERME_IN_GA(.(T45, T46), .(T47, T48)) → APPEND2A_IN_AAAG(X68, T47, X69, T46)
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → U1_AAAG(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → APPEND2A_IN_AAAG(X107, T79, X108, T78)
PERME_IN_GA(.(T45, T46), .(T47, T55)) → U8_GA(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → APPEND1D_IN_GGGA(T45, T53, T54, X27)
APPEND1D_IN_GGGA(T93, T94, T95, .(T93, X134)) → U3_GGGA(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
APPEND1D_IN_GGGA(T93, T94, T95, .(T93, X134)) → APPEND1B_IN_GGA(T94, T95, X134)
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → U2_GGA(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → APPEND1B_IN_GGA(T110, T111, X156)
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_GA(T45, T46, T47, T55, permE_in_ga(T84, T55))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U4_GA(T27, T28, T29, append1C_in_ga(T28, X27))
PERME_IN_GA(.(T27, T28), .(T27, T29)) → APPEND1C_IN_GA(T28, X27)
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U5_GA(T27, T28, T29, append1C_in_ga(T28, T31))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_GA(T27, T28, T29, permE_in_ga(T31, T29))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(.(T45, T46), .(T47, T48)) → U7_GA(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
PERME_IN_GA(.(T45, T46), .(T47, T48)) → APPEND2A_IN_AAAG(X68, T47, X69, T46)
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → U1_AAAG(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → APPEND2A_IN_AAAG(X107, T79, X108, T78)
PERME_IN_GA(.(T45, T46), .(T47, T55)) → U8_GA(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → APPEND1D_IN_GGGA(T45, T53, T54, X27)
APPEND1D_IN_GGGA(T93, T94, T95, .(T93, X134)) → U3_GGGA(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
APPEND1D_IN_GGGA(T93, T94, T95, .(T93, X134)) → APPEND1B_IN_GGA(T94, T95, X134)
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → U2_GGA(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → APPEND1B_IN_GGA(T110, T111, X156)
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_GA(T45, T46, T47, T55, permE_in_ga(T84, T55))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → APPEND1B_IN_GGA(T110, T111, X156)
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
APPEND1B_IN_GGA(.(T109, T110), T111, .(T109, X156)) → APPEND1B_IN_GGA(T110, T111, X156)
APPEND1B_IN_GGA(.(T109, T110), T111) → APPEND1B_IN_GGA(T110, T111)
From the DPs we obtained the following set of size-change graphs:
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → APPEND2A_IN_AAAG(X107, T79, X108, T78)
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
APPEND2A_IN_AAAG(.(T77, X107), T79, X108, .(T77, T78)) → APPEND2A_IN_AAAG(X107, T79, X108, T78)
APPEND2A_IN_AAAG(.(T77, T78)) → APPEND2A_IN_AAAG(T78)
From the DPs we obtained the following set of size-change graphs:
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U5_GA(T27, T28, T29, append1C_in_ga(T28, T31))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(.(T45, T46), .(T47, T55)) → U8_GA(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T27, T28), .(T27, T29)) → U4_ga(T27, T28, T29, append1C_in_ga(T28, X27))
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
U4_ga(T27, T28, T29, append1C_out_ga(T28, X27)) → permE_out_ga(.(T27, T28), .(T27, T29))
permE_in_ga(.(T27, T28), .(T27, T29)) → U5_ga(T27, T28, T29, append1C_in_ga(T28, T31))
U5_ga(T27, T28, T29, append1C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(.(T45, T46), .(T47, T48)) → U7_ga(T45, T46, T47, T48, append2A_in_aaag(X68, T47, X69, T46))
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U7_ga(T45, T46, T47, T48, append2A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(.(T45, T46), .(T47, T48))
permE_in_ga(.(T45, T46), .(T47, T55)) → U8_ga(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, X27))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
U9_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(.(T45, T46), .(T47, T55))
U8_ga(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(.(T45, T46), .(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(.(T27, T28), .(T27, T29))
PERME_IN_GA(.(T27, T28), .(T27, T29)) → U5_GA(T27, T28, T29, append1C_in_ga(T28, T31))
U5_GA(T27, T28, T29, append1C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(.(T45, T46), .(T47, T55)) → U8_GA(T45, T46, T47, T55, append2A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, append2A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, append1D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, append1D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
append1C_in_ga(T37, T37) → append1C_out_ga(T37, T37)
append2A_in_aaag([], T68, T69, .(T68, T69)) → append2A_out_aaag([], T68, T69, .(T68, T69))
append2A_in_aaag(.(T77, X107), T79, X108, .(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, append2A_in_aaag(X107, T79, X108, T78))
append1D_in_ggga(T93, T94, T95, .(T93, X134)) → U3_ggga(T93, T94, T95, X134, append1B_in_gga(T94, T95, X134))
U1_aaag(T77, X107, T79, X108, T78, append2A_out_aaag(X107, T79, X108, T78)) → append2A_out_aaag(.(T77, X107), T79, X108, .(T77, T78))
U3_ggga(T93, T94, T95, X134, append1B_out_gga(T94, T95, X134)) → append1D_out_ggga(T93, T94, T95, .(T93, X134))
append1B_in_gga([], T102, T102) → append1B_out_gga([], T102, T102)
append1B_in_gga(.(T109, T110), T111, .(T109, X156)) → U2_gga(T109, T110, T111, X156, append1B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, append1B_out_gga(T110, T111, X156)) → append1B_out_gga(.(T109, T110), T111, .(T109, X156))
PERME_IN_GA(.(T27, T28)) → U5_GA(append1C_in_ga(T28))
U5_GA(append1C_out_ga(T31)) → PERME_IN_GA(T31)
PERME_IN_GA(.(T45, T46)) → U8_GA(T45, append2A_in_aaag(T46))
U8_GA(T45, append2A_out_aaag(T53, T47, T54)) → U10_GA(append1D_in_ggga(T45, T53, T54))
U10_GA(append1D_out_ggga(T84)) → PERME_IN_GA(T84)
append1C_in_ga(T37) → append1C_out_ga(T37)
append2A_in_aaag(.(T68, T69)) → append2A_out_aaag([], T68, T69)
append2A_in_aaag(.(T77, T78)) → U1_aaag(T77, append2A_in_aaag(T78))
append1D_in_ggga(T93, T94, T95) → U3_ggga(T93, append1B_in_gga(T94, T95))
U1_aaag(T77, append2A_out_aaag(X107, T79, X108)) → append2A_out_aaag(.(T77, X107), T79, X108)
U3_ggga(T93, append1B_out_gga(X134)) → append1D_out_ggga(.(T93, X134))
append1B_in_gga([], T102) → append1B_out_gga(T102)
append1B_in_gga(.(T109, T110), T111) → U2_gga(T109, append1B_in_gga(T110, T111))
U2_gga(T109, append1B_out_gga(X156)) → append1B_out_gga(.(T109, X156))
append1C_in_ga(x0)
append2A_in_aaag(x0)
append1D_in_ggga(x0, x1, x2)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
append1B_in_gga(x0, x1)
U2_gga(x0, x1)
PERME_IN_GA(.(T27, T28)) → U5_GA(append1C_in_ga(T28))
U5_GA(append1C_out_ga(T31)) → PERME_IN_GA(T31)
PERME_IN_GA(.(T45, T46)) → U8_GA(T45, append2A_in_aaag(T46))
U8_GA(T45, append2A_out_aaag(T53, T47, T54)) → U10_GA(append1D_in_ggga(T45, T53, T54))
U10_GA(append1D_out_ggga(T84)) → PERME_IN_GA(T84)
append1C_in_ga(T37) → append1C_out_ga(T37)
append2A_in_aaag(.(T68, T69)) → append2A_out_aaag([], T68, T69)
append2A_in_aaag(.(T77, T78)) → U1_aaag(T77, append2A_in_aaag(T78))
append1D_in_ggga(T93, T94, T95) → U3_ggga(T93, append1B_in_gga(T94, T95))
U1_aaag(T77, append2A_out_aaag(X107, T79, X108)) → append2A_out_aaag(.(T77, X107), T79, X108)
U3_ggga(T93, append1B_out_gga(X134)) → append1D_out_ggga(.(T93, X134))
append1B_in_gga([], T102) → append1B_out_gga(T102)
append1B_in_gga(.(T109, T110), T111) → U2_gga(T109, append1B_in_gga(T110, T111))
U2_gga(T109, append1B_out_gga(X156)) → append1B_out_gga(.(T109, X156))
U10GA1 > append1Dinggga3 > append2Ainaaag1 > append1Coutga1 > .2 > U5GA1 > PERMEINGA1 > U1aaag2 > U8GA2 > append1Bingga2 > U2gga2 > U3ggga2 > append1Doutggga1 > append1Boutgga1 > [] > append2Aoutaaag3 > append1Cinga1
[]=4
append1C_in_ga_1=3
append1C_out_ga_1=2
append2A_in_aaag_1=3
append1B_out_gga_1=4
append1D_out_ggga_1=3
PERME_IN_GA_1=3
U5_GA_1=1
U10_GA_1=1
._2=1
append2A_out_aaag_3=0
U1_aaag_2=1
append1D_in_ggga_3=0
U3_ggga_2=0
append1B_in_gga_2=0
U2_gga_2=1
U8_GA_2=1
append1C_in_ga(x0)
append2A_in_aaag(x0)
append1D_in_ggga(x0, x1, x2)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
append1B_in_gga(x0, x1)
U2_gga(x0, x1)